/*
 * $Id: FractalRuntimeChecker.java 1259 2007-01-09 14:23:47Z tcoupaye $
 *
 * Behavior Protocols extensions for static and runtime checking
 * developed for the Julia implementation of Fractal.
 *
 * Copyright (C) 2006
 *    Formal Methods In Software Engineering Group
 *    Institute of Computer Science
 *    Academy of Sciences of the Czech Republic
 *
 * Copyright (C) 2006 France Telecom
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307 USA
 *
 * Contact: ft@nenya.ms.mff.cuni.cz
 * Authors: Jan Kofron <kofron@nenya.ms.mff.cuni.cz>
 */

package org.objectweb.fractal.bpc.checker;

import java.io.IOException;
import java.io.OutputStream;

import org.objectweb.fractal.bpc.checker.DFSR.CheckingException;
import org.objectweb.fractal.bpc.checker.DFSR.Options;
import org.objectweb.fractal.bpc.checker.node.ActionRepository;
import org.objectweb.fractal.bpc.checker.node.DeterministicNode;
import org.objectweb.fractal.bpc.checker.node.InvalidParameterException;
import org.objectweb.fractal.bpc.checker.node.TreeNode;
import org.objectweb.fractal.bpc.checker.parser.Builder;
import org.objectweb.fractal.bpc.checker.parser.StringTokenizer;
import org.objectweb.fractal.bpc.checker.parser.SyntaxErrorException;
import org.objectweb.fractal.bpc.checker.state.Signature;
import org.objectweb.fractal.bpc.checker.state.State;
import org.objectweb.fractal.bpc.checker.state.TransitionPair;
import org.objectweb.fractal.bpc.checker.utils.ProtocolUsageMonitor;

/**
 * This class accept information about runtime behavior of a component and
 * checks, whether it corresponds with a given protocol.
 */
public class FractalRuntimeChecker {

    /**
     * Creates a new instance of FractalRuntimeChecker.
     * @param protocol protocol of the component to be watched
     * @param monitorusage true if the protocol should be watched for used events
     * @throws SyntaxErrorException if a syntax error is found during parsing the protocols.
     */
    public FractalRuntimeChecker(String protocol, boolean monitorusage) throws SyntaxErrorException {
        repository = new ActionRepository();
        node = new DeterministicNode(new Builder(repository).build(new StringTokenizer(protocol), true));
        
        if (node != null)
	          Signature.setSize(node.getLeafCount());

        currentState = node.getInitial();
        
        Options.monitorusage = monitorusage;
    }

    /**
     * Accepts the notification about a method call requests or responds.
     * 
     * @param event
     *            event being performed
     * @return the type of the error, zero = no error
     */
    public int notify(String event) {
    
		synchronized(FractalRuntimeChecker.class) {
	
			boolean found = false;
			//extract the index of this event
			int action;
			
			try {
				  action = repository.getItemIndex(event);
			}
			catch (NullPointerException e) {
					return ERR_BADACTIVITY;
			}
				
			TransitionPair[] transitions = null;
	
			// obtain all possible transitions
			try {
				transitions = node.getTransitions(currentState).transitions;
			} catch (InvalidParameterException e) {
				//shouldn't appear
				System.out.println("Internal Checker Error - InvalidParameterException");
				e.printStackTrace();
				return -1;
			} catch (CheckingException e) {
				//shouldn't appear
				System.out.println("Internal Checker Error - CheckingException");
				e.printStackTrace();
				return -1;
			}
	
			//find the real transitions within the set of possible transitions
			for (int i = 0; i < transitions.length; ++i) {
				if (transitions[i].eventIndex == action) {
					currentState = transitions[i].state;
					found = true;
					if (Options.monitorusage)
						ProtocolUsageMonitor.eventExecuted(transitions[i].eventIndex);
					
					break;
				}
			}
	
			if (!found) // bad activity
				return ERR_BADACTIVITY;
			else
				return ERR_OK;
		}

    }

    /**
     * Tests, if the execution is finished at this state.
     * 
     * @return true iff the current state is accepting (i.e. a trace ends with
     *         this event)
     */
    public boolean isAccepting() {
        return node.isAccepting(currentState);
    }
    

    /**
     * Writes a html file with protocol usage 
     * @param out the output stream to write to 
     * @throws IOException in case of an error when writing to the stream
     */
    public void writeUsageFile(OutputStream out) throws IOException {
        ProtocolUsageMonitor.printUsage(out, node);
    }

    /**
     * current state within the state space
     */
    private State currentState;

    /**
     * the top of the parse tree automaton
     */
    private TreeNode node;

    /**
     * The action repository
     */
    private ActionRepository repository;
    
    /**
     * Return types of error
     */
    public static int ERR_OK = 0;

    public static int ERR_BADACTIVITY = 1;
}
